forall a: forall b: forall c:
forall Q:a->b:
Q;O:b,c = O:a,c